00100	FINITIZATION OF THEORIES (A research topic)
00200	
00300	
00400		A first order theory ⊗T is particularly easy to handle if
00500	it has the following property which we call ⊗boundability.
00600	A sentence ⊗p is valid in ⊗T iff if it is true in all models of
00700	some fixed size ⊗N.  Obviously boundable theories are decidable
00800	and if ⊗N is small, then ⊗T is readily decidable.
00900	
01000		Now boundable theories are not very common, but it may
01100	be possible to convert the problem of deciding certain sentences
01200	in unboundable theories into decision problems in boundable theories.
01300	I am particularly interested in questions of satisfiability.
01400	
01500		My intuition that this may sometimes be possible comes
01600	from the following circumstance.  Suppose you ask someone to
01700	give a model of  certain sentence.  He says something like,
01800	%2"Let A = IXI where I is the set of integers and let f: A → I
01900	be defined as follows: etc."%1  He actually gives his model
02000	by mentioning only a finite number of objects, but some of them
02100	are infinite sets.  Now perhaps there is a theory in which
02200	the set of integers is an object, but the individual integers
02300	are not, and perhaps ⊗p can be translated into a sentence ⊗p' 
02400	in that theory, and perhaps that theory is boundable.
02500	
02600		There are two remarks: First category theory starts
02700	out with sets and functions, so some small piece of category
02800	theory may be what we want.
02900	
03000		Second, we may want a notion of ⊗truncation of a theory.
03100	The idea is that we can truncate the integers by making all
03200	integers greater than say 50 undefined and truncate LISP by
03300	making all lists longer than 10 or of depth greater than 3
03400	undefined.
03500	The idea is that to model some sentences we may need only
03600	truncated theories.